A:Type, eq:EqDecider(A), x,y:A, v,z:top.
sqequal(fpf-cap(fpf-single(x; v); eq; y; z); if eqof(eq)(x,y) then v else z fi ) 

latex

Definitions	x:A. B(x), fpf-cap(f; eq; x; z), fpf-single(x; v), if b then t else f fi , fpf-dom(eq; x; f), fpf-ap(f; eq; x), t.2, deq-member(eq; x; L), t.1, reduce(f; k; as), ff, Y, t  T, P  Q, tt, P  Q, b, P  Q, prop{i:l}, True, P  Q, P  Q, b, T, , Unit, False, A,
Lemmas	bor wf, eqof wf, bfalse wf, bool wf, iff transitivity, assert wf, false wf, eqtt to assert, assert of bor, bnot wf, not wf, eqff to assert, assert of bnot, band wf, btrue wf, true wf, squash wf, bnot thru bor, assert of band, and functionality wrt iff, top wf, deq wf